FDL - Step of Proof: less-fast-fib

Step of Proof: less-fast-fib

11,40

Inference at * 2 1 1
Iof proof for Lemma less-fast-fib:

1. f :
1.

n, a, b:

.
1. {m:

|
1. {

. (a = fib(k))

((k

(b = 0))

((0 < k)

(b = fib(k - 1)))

(m = fib(n+k))}

(

n.f(n,1,0))

(

. {m:

| m = fib(n)} )

by (RepeatFor (first_nat 1:n) ((MemCD)

CollapseTHENA (Auto

)

))

C1: .....subterm..... T:t1:n

C1: 2. n :

C1:

f(n,1,0)

{m:

| m = fib(n)}

Definitions x.A(x), x:A. B(x), t T,

Lemmas nat wf